(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(** ** Block Matrix Transpose *)
Require Export List.
Require Export Matrix.Mat.Matrix_Module.
Require Import Matrix.MMat.MMat_def.
Require Import Matrix.MMat.Mlist_function.


Import ListNotations.

(* ################################################################# *)
(** * Definition of Matrix Transpose *)



Section Mat_trans.

Variable A:Set.
Variable Zero:A.
Variable m n p:nat.

Definition mhead (l:list(@Mat A m n)):=
  match l with
  | [] => trans A Zero (MO A Zero m n)
  | x::_ =>trans A Zero x
  end.


(** *** headcolumn *)
(** Get the first column of the two-dimensional list. *)
Fixpoint mheadcolumn (ma:list (list (@Mat A m n))) :=
  match ma with
  | nil => nil
  | cons x x' => (mhead x)::(mheadcolumn x')
  end.

Lemma length_mheadcolumn : forall n2 l,
  length l = n2 -> length (mheadcolumn l ) = n2.
Proof.
  induction n2. induction l. auto.
  intros. inversion H. induction l. intros. inversion H.
  intros. simpl. f_equal. apply IHn2. inversion H. auto.
Qed.

(** *** gettrans *)
(** Transpose the two-dimensional list of width n. *)
Fixpoint mgettrans(ma:list (list (@Mat A m n))) (n2:nat):=
  match n2 with
  | O => nil
  | S n' => (mheadcolumn ma)
            ::(mgettrans (tailcolumn (@Mat A m n) ma) n')
  end.

Lemma mat_mhead: forall a,
  mat A n m (mhead a) =
  gettrans A Zero (headcolumn_n A Zero (lM_to_M1 a) n) n.
Proof.
  induction a. simpl. f_equal. rewrite headcolumn_n_nil_list. auto.
  simpl. f_equal. rewrite headcolumn_n_mlink with(h:=m).
  auto. apply (mat_height A m n a). apply height_lM_to_M1.
  apply (mat_width A m n a).
Qed. 

Lemma mgettrans_nil :  forall n2 ,
  mgettrans nil n2 = nil_list (Mat A n m) n2.
Proof. induction n2.
  simpl. auto. simpl. f_equal. apply IHn2.
Qed.

Lemma height_mgettrans : forall n2 ma,
  width ma n2 -> height (mgettrans ma n2) = n2.
Proof.
  induction n2. simpl. auto.
  induction ma. intros. rewrite mgettrans_nil.
  apply height_nil_list. intros. simpl. f_equal.
  apply IHn2. simpl. split. apply length_tl. apply H.
  apply width_tailcolumn. apply H.
Qed.

Lemma width_mgettrans : forall m2 n2 ma,
  height ma = m2-> width ma n2 ->
  width (mgettrans ma n2 ) m2.
Proof.
  induction m2. induction n2. simpl. auto.
  intros. simpl. split. apply length_mheadcolumn. 
  auto. apply IHn2. apply height_tailcolumn. auto.
  apply width_tailcolumn. auto.
  induction n2. induction ma. intros. inversion H.
  intros. simpl. auto. induction ma. intros.
  inversion H. intros. simpl. split. f_equal.
  apply length_mheadcolumn. inversion H. auto.
  apply IHn2. simpl. f_equal. apply height_tailcolumn.
  inversion H. auto. simpl. split. apply length_tl.
  apply H0. apply width_tailcolumn. apply H0.
Qed.

Definition mmtrans{m2 n2}(mma:Mat(Mat A m n) m2 n2):=
  mkMat (Mat A n m) n2 m2 (mgettrans (mat (Mat A m n) m2 n2 mma) n2)
  (height_mgettrans n2 (mat (Mat A m n) m2 n2 mma) (mat_width (Mat A m n) m2 n2 mma))
  (width_mgettrans m2 n2 (mat (Mat A m n) m2 n2 mma) 
  (mat_height (Mat A m n) m2 n2 mma) (mat_width (Mat A m n) m2 n2 mma)).

End Mat_trans.

Section Lemma.

Variable A:Set.
Variable Zero:A.

(*
Lemma dl_elem_trans_nil_list: forall m2 m n,
  dl_elem_trans A Zero m n (nil_list (Mat A m n) m2) = nil_list (Mat A n m) m2.
Proof.
  induction m2. simpl. auto. simpl. intros. f_equal. apply IHm2.
Qed.
*)

Variable m n p:nat.

Fixpoint l_to_dl(l:list (Mat A m n)):=
  match l with
  | nil => nil
  | x :: x' => (x::nil)::(l_to_dl x')
  end.
 
    

 

Lemma tailcolumn_n_lM_to_M1: forall (a:list(Mat A m n)),
  tailcolumn_n A (lM_to_M1 a) n  = lM_to_M1(tl a).
Proof.
  induction a. simpl. rewrite tailcolumn_n_nil_list. auto.
  simpl. rewrite tailcolumn_n_mlink with(h:= m). auto.
  apply (mat_height A m n a). apply height_lM_to_M1.
  apply (mat_width A m n a).
Qed.

Lemma tailcolumn_n_dlM_to_M1 : forall (ma:list(list (Mat A m n))) ,
  tailcolumn_n A (dlM_to_M1 ma) n = dlM_to_M1 (tailcolumn (Mat A m n) ma).
Proof.
  induction ma. simpl. auto.
  simpl. rewrite tailcolumn_n_app. f_equal. apply tailcolumn_n_lM_to_M1.
  apply IHma.
Qed.





Lemma headcolumn_n_lM_to_M1: forall m n (a:list(Mat A m n)), 
  headcolumn_n A Zero (lM_to_M1 a) n
  = mat A m n (@hd (Mat A m n) (MO A Zero m n) a).
Proof.
  induction a.
  simpl. rewrite headcolumn_n_nil_list. auto.
  simpl. rewrite headcolumn_n_mlink with(h:= m0). 
  auto. apply (mat_height A m0 n0 a).
  apply height_lM_to_M1. apply (mat_width A m0 n0 a).
Qed.

Lemma lM_to_M1_mheadcolumn: forall h ma,
  length ma = h ->
  lM_to_M1 (mheadcolumn A Zero m n ma) =
  gettrans A Zero (headcolumn_n A Zero (dlM_to_M1 ma) n) n.
Proof.
  induction h.
  - induction ma. simpl. rewrite gettrans_nil. auto.
    intros. inversion H.
  - induction ma. intros. inversion H.
    intros. simpl. rewrite headcolumn_n_app with(h1:= m)(h2:=h*m).
    rewrite gettrans_app_mlink with (h1:= m)(h2:=h*m).
    f_equal. apply mat_mhead. apply IHh. inversion H. auto.
    apply height_headcolumn_n. apply height_lM_to_M1.
    apply height_headcolumn_n. apply height_dlM_to_M1.  
    inversion H. auto. apply width_headcolumn_n.
    apply width_headcolumn_n. apply height_lM_to_M1.
    apply height_dlM_to_M1. inversion H. auto.
Qed.

Lemma dlM_to_M1_mgettrans: forall h w (ma:list (list (Mat A m n))),
   height ma = h -> width ma w ->
  dlM_to_M1 (mgettrans A Zero m n ma w) =
  gettrans A Zero (dlM_to_M1 ma) (w * n).
Proof.
  induction h. - induction w. * simpl. auto.
    * intros. simpl. rewrite gettrans_app. f_equal.
    apply lM_to_M1_mheadcolumn with(h:=0). auto.
    rewrite tailcolumn_n_dlM_to_M1. apply IHw. apply height_tailcolumn.
    auto. apply width_tailcolumn. apply H0. assert(n+w*n =(S w)*n).
    { auto. } rewrite H1. apply width_dlM_to_M1. apply H0.
    apply width_headcolumn_n. apply width_tailcolumn_n.
    assert(n+w*n =(S w)*n). { auto. } rewrite H1.
    apply width_dlM_to_M1. apply H0.
  - induction w.
    * simpl. auto.
    * induction ma. intros. inversion H. intros.
      simpl. rewrite gettrans_app. f_equal.
      rewrite headcolumn_n_app with(h1:=m)(h2:=h*m).
      rewrite gettrans_app_mlink with(h1:=m)(h2:=h*m).
      f_equal. apply mat_mhead. apply lM_to_M1_mheadcolumn with(h:=h).
      inversion H. auto. apply height_headcolumn_n. apply height_lM_to_M1.
      apply height_headcolumn_n. apply height_dlM_to_M1. inversion H. auto.
      apply width_headcolumn_n. apply width_headcolumn_n.
      apply height_lM_to_M1. apply height_dlM_to_M1. inversion H. auto.
      rewrite tailcolumn_n_app. rewrite IHw. f_equal.
      rewrite <- tailcolumn_n_app. 
      assert(tl a :: tailcolumn (Mat A m n) ma =
      tailcolumn (Mat A m n) (a::ma)). { auto. }
      rewrite H1. assert(lM_to_M1 a ++ dlM_to_M1 ma=dlM_to_M1(a::ma)).
      { auto. } rewrite H2.  rewrite tailcolumn_n_dlM_to_M1.
      auto. simpl. f_equal. apply height_tailcolumn. inversion H.
      auto. simpl. split. apply length_tl. apply H0.
      apply width_tailcolumn. apply H0. apply width_app.
      assert(n+w*n =(S w)*n). { auto. }
      split. rewrite H1. apply width_lM_to_M1. apply H0. rewrite H1.
      apply width_dlM_to_M1. apply H0. apply width_headcolumn_n.
      apply width_tailcolumn_n. apply width_app.   
      assert(n+w*n =(S w)*n). { auto. } split.
      rewrite H1. apply width_lM_to_M1. apply H0. rewrite H1.
      apply width_dlM_to_M1. apply H0.
Qed.

Variable m2 n2:nat.
Variable me:Mat (Mat A m n) m2 n2.

Lemma MMtrans_eq_Mtrans: 
  MM_to_M(mmtrans A Zero m n me) === trans A Zero (MM_to_M me).
Proof.
  unfold MM_to_M,mmtrans,trans,M_eq. simpl.
  induction me.
  unfold MM_to_M'. simpl.
  apply dlM_to_M1_mgettrans with (h:= m2). auto. auto.
Qed.

End Lemma.

Section mmtrans_lemma.

Variable A:Set.
Variable Zero:A.
Variable m n m2 n2: nat.

Lemma mmtrans_same:forall(ma:Mat (Mat A m n) m2 n2),
  mmtrans A Zero n m (mmtrans A Zero m n ma) == ma.
Proof.
  intros.
  rewrite MM_to_M_M_eq.
  rewrite ?MMtrans_eq_Mtrans. apply trans_same.
  apply (mat_height A (m2*m) (n2*n) (MM_to_M ma)).
  apply (mat_width A (m2*m) (n2*n) (MM_to_M ma)).
Qed.

Lemma mmteq_f: forall f (ma mb:Mat (Mat A m n) m2 n2),
  (forall a : A, f a Zero = a)->
  mmtrans A Zero m n 
  (matrix_each (Mat A m n) (matrix_each A f) ma mb)==
  matrix_each (Mat A n m) (matrix_each A f ) 
  ( mmtrans A Zero m n ma) ( mmtrans A Zero m n mb).
Proof.
  intros.
  rewrite MM_to_M_M_eq. rewrite ?MMtrans_eq_Mtrans.
  rewrite ?MM_to_M_matrix_each. rewrite ?MMtrans_eq_Mtrans.
  apply teq_add. auto. auto. auto.
Qed.

End mmtrans_lemma.
